Definitions | Id, t T, {x:A| B(x)} , Knd, b, Top, left + right, x:A B(x), x:A. B(x), State(ds), Type, x:A B(x), hasloc(k;i),  x. t(x), a:A fp B(a), x.A(x), MaInterface(T), ES, P  Q, ma-interface-consistent-at(es;i;X), IdDeq, x dom(f), , ma-interface-consistent(es;X) |